package struct;
import java.util.ArrayList;

public class Unifier {

    private Rule toSolve;
	private ArrayList<Rule> rules;
	private ArrayList<Rule> oldRules;
	private Identity lastSubst;
    int max;
    
    public int getMax() {
        return max;
    }

    public void setMax(int max) {
        this.max = max;
    }

    public Unifier() {
        rules = new ArrayList<Rule>();
        oldRules = new ArrayList<Rule>();
    }
    
    public ArrayList<Rule> getRules()
    {
        return rules;
    }
    
    public void clearRules()
    {
        rules.clear();
        oldRules.clear();
    }
    
    public Rule getToSolve()
    {
    	return toSolve;
    }

    public void solve(Rule rule)
    {
    	if (delete(rule))
        {
            //rule not added to rules list
    		//solve finishes, nothing more to do.
        }
        else
        {
        	if (eliminate(rule))
        	{
        		if (needsOrienting(rule)) //it needs orienting
        		{
        			rule = orient(rule);
        		}
        		
        		if (!rules.contains(rule) && !oldRules.contains(rule))
        		{
        		    substituteRules(rule);
        			rules.add(rule);
        		}
        	}

        	decompose(rule);
        	
        }
    }
    
    private void substituteRules(Rule rule) {
    	lastSubst = rule.getRight().getTerm();
    	
    	for (int i = 0; i < rules.size(); i++)
    	{
    	    Rule oldRule = (Rule)rules.get(i).clone();
    		rules.get(i).getLeft().setTerm(
    				trySubstitute(rules.get(i).getLeft().getTerm(), rule.getLeft().getTerm()));
    		rules.get(i).getRight().setTerm(
    				trySubstitute(rules.get(i).getRight().getTerm(), rule.getLeft().getTerm()));
    		
    		if (delete(rules.get(i)))
    		{
    		    if (!oldRules.contains(oldRule))
    		    {
    		        oldRules.add(oldRule);
    		    }
    		    rules.remove(i);
    		}
    	}
		
	}

	private Identity trySubstitute(Identity i1, Identity i2) {

		if (i1.toString().contains(i2.toString()))
		{
			if (i1.equals(i2))
			{
				return lastSubst;
			}
			else if (i1 instanceof Function)
			{
				Function func = (Function) i1;
				for (int i = 0; i < func.getArgs().length; i++)
				{
					func.setArg(trySubstitute(func.getArg(i), i2), i);
				}
				return func;
			}
		}
		return i1;
	}

	private boolean delete(Rule rule)
    {
        Identity left = rule.getLeft().getTerm();
        Identity right = rule.getRight().getTerm();
        if (left instanceof Function && right instanceof Function)
        {
            if ((((Function)left).equals(((Function)right))))
            {
                return true;
            }
        }
        else if (left instanceof Variable && right instanceof Variable)
        {
            if ((((Variable)left).equals(((Variable)right))))
            {
                return true;
            }
        }
        return false;
    }
    
    private void decompose(Rule rule)
    {
        Identity left = rule.getLeft().getTerm();
        Identity right = rule.getRight().getTerm();
        
        if ((left instanceof Function && right instanceof Function) && 
            (((Function)left).getName() == ((Function)right).getName()) &&
            (((Function)left).getArgs().length == ((Function)right).getArgs().length))
        {
            Function fleft = (Function) left;
            Function fright = (Function) right;
            
            for (int i = 0; i < fleft.getArgs().length; i++)
            {
                Term t1 = new Term(fleft.getArgs()[i]);
                Term t2 = new Term(fright.getArgs()[i]);
                Rule newRule = new Rule(t1, t2);
                solve(newRule);
            }
        }
    }
    
    private Rule orient(Rule rule)
    {
        return new Rule(rule.getRight(), rule.getLeft());
    }
    
    private boolean eliminate(Rule rule)
    {
        Identity left = rule.getLeft().getTerm();
        Identity right = rule.getRight().getTerm();
        
        if (left.getMaxIndex() != right.getMaxIndex())
        {
            return true;
        }
        else
        {
            return false;
        }
    }
    
    private boolean needsOrienting(Rule rule)
    {
        Identity left = rule.getLeft().getTerm();
        Identity right = rule.getRight().getTerm();
        
        if (left.getMaxIndex() == max + 1 && right.getMaxIndex() == max)
        {
            return false;
        }
        else
        {
            return true;
        }
    }
}
